Not Applicable.
Not Applicable.
This invention relates to electronic design automation, specifically to verification of electronic circuit designs"" functional correctness using a computer program.
A digital circuit includes gates, memory elements and wires connecting the gates and the memory elements. When people make a large digital circuit design, they write the design in a hardware description language. IEEE standards 1076 and 1364 are 2 well-known hardware description languages. Identifiers in a hardware description language are used to represent wires and memory elements in circuits. An identifier can be called a wire if its value at any circuit operation time does not directly depend on its value at a previous circuit operation time. An identifier can be called a memory element if its value at a circuit operation time is simply its value at a previous circuit operation time. For the purpose of avoiding erroneous chips, they have to verify that the design is functionally correct before transforming the design into a format used for fabricating the chip. As chips growing larger and larger, the existing verification methods are no longer able to guarantee their functional correctness.
A method to verify functional correctness is to use a logic simulator, and this is called directed simulation in the following discussion. The simulator reads the circuit design and a set of stimulus values for the inputs of the circuit design. The simulator then computes the circuit design""s response behavior. The circuit design""s functional correctness is decided by comparing the computed response behavior with the expected behavior. The description of both the stimulus values and the correctness decision logic is generally called a test bench. The identifiers in this description can also be called wires or memory elements as in a hardware description language. In fact, this description is usually in a hardware description language.
The values used for a logic simulator normally include 0 and 1. They sometimes include a high impedance value, which is usually called Z. Other values may also be included in some cases to indicate values between 0, 1 and Z, and they are often called values of different strengths. A special value, usually called X, is sometimes included to indicate an unknown value (or an abnormal value). How gates and memory elements respond to these values other than 0 and 1 is defined to be meaningful in most cases, but it may not work meaningfully for all cases. In many cases, the gates or memory elements simply produce X values for such difficult cases. If a signal does not get any value, its default value is obtained according to some predefined rules.
This method using logic simulators can handle nearly all cases but it is not efficient because too many simulation runs are required for a large design and a lot of computation in the simulator is repeated too many times. The stimulus values can be automatically generated by a pseudo-random number generator or they can be generated by exhaustively enumerating through all possible combinations, but these generation approaches do not solve these efficiency problems.
Another method to verify functional correctness is to analyzing the design against an assertion (or a property). It usually involves transforming the design and the assertion from one representation to another before analyzing whether the design satisfies the assertion. The analysis generally treats the design and the assertion as equations of Boolean variables. The analysis can be done in several different ways, which are usually called formal methods or symbolic methods. In the following discussion, they are called symbolic analysis processes. These processes are highly efficient but they can be applied to only a limited subset of the real world verification problems. This limitation is the result of the great computational complexities of general verification problems, and these formal or symbolic methods are used to find complete solution to these complex problems.
There are needs for incomplete and efficient solutions to the functional verification tasks. Because of the incompleteness of these solutions, convenient and flexible methods are needed for users to specify subsets of these verification tasks. These methods should also make it easy for users to adjust these subsets. They are made possible by patent applications Ser. No. 09/257,148 titled Hybrid Method for Design Verification and Ser. No. 09/531,633 titled Method for Conditional Tautology Checking together.
The present invention provides a method for verifying a digital circuit design in a hardware description language, using a test bench template and a verification process. A test bench feeds values to the signals in the circuit design and reads the response behavior from the circuit design. The test bench template is an incompletely specified test bench which includes a checking function and may feed no values, X values and Z values in addition to 0 values and 1 values to certain signals. The verification process treats no values and X values as changing wild cards. A changing wild card can change between 0 and 1 at any circuit operation time in simulation. The verification process completely covers all possible permutations of 0/1 binary values for these changing wild cards.
This method works with both logic simulation and formal (or symbolic) methods. It also allows making trade-off decisions both manually by users and automatically by the verification process. Therefore this method makes it easy to optimize the solutions to the verification tasks.